Nuprl Lemma : bool-to-dcdr-aux
11,40
postcript
pdf
A
:Type,
f
:(
A
),
x
:
A
. Dec(
f
(
x
) = tt)
latex
ProofTree
Definitions
Dec(
P
)
,
s
=
t
,
x
:
A
.
B
(
x
)
,
f
(
a
)
,
tt
,
x
:
A
B
(
x
)
,
,
t
T
,
Type
Lemmas
bool
wf
,
btrue
wf
,
decidable
equal
bool
origin
A:Type, f:(A
), x:A. Dec(f(x) = tt)
A:Type, f:(A), x:A. Dec(f(x) = tt)
x:A. B(x)B(x)
T